Nuprl Lemma : ESAtomAxiom_wf
0,22
postcript
pdf
T
:(Id
Id
Type{i}),
V
:(Id
Knd
Type{i}). ESAtomAxiom{i:l}(
T
;
V
)
Prop{i'}
latex
Definitions
Type
,
t
T
,
Id
,
x
:
A
B
(
x
)
,
Knd
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
AtomFree(
T
;
x
)
,
Prop
,
x
:
A
B
(
x
)
,
P
&
Q
,
ESAtomAxiom{i:l}(
T
;
V
)
Lemmas
atom-free
wf
,
Knd
wf
,
Id
wf
origin
T:(Id
IdType{i}), V:(IdKndType{i}). ESAtomAxiom{i:l}(T; V) 
Prop{i'} T:(IdIdType{i}), V:(IdKndType{i}). ESAtomAxiom{i:l}(T; V) Prop{i'} TB(x)x:A. B(x)
B(x)